;;;===========================================================================
;;;
;;; Direct Sum construction
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 01/06/10 || End date: 01/06/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "algebraic-data-structures")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring *) => *)
 ;; Addition operation ring
 ((addition-ring * *)=> *)
 ;; Product operation ring
 ((product-ring * *) => *)
 ;; Inverse ring
 ((inverse *) => *)
 ;; Zero element ring
 ((zero-element ) => *)
 ;; Unit element ring
 ((unit )=> *)

 ;;--------------------------------------------------
 ;; D Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-D * *) => *)
 ;; Group Operation 
 ((group-operation-D * * *) => *)
 ;; Zero element
 ((zero-D *) => *)
 ;; External multiplication
 ((external-D * * *) => *)
 ;; Inverse element
 ((inverse-D * *) => *)

 ;;--------------------------------------------------
 ;; The D differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-D * *) => *)
 


 ;;--------------------------------------------------
 ;; C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C * *) => *)
 ;; Group Operation 
 ((group-operation-C * * *) => *)
 ;; Zero element
 ((zero-C *) => *)
 ;; External multiplication
 ((external-C * * *) => *)
 ;; Inverse element
 ((inverse-C * *) => *)

 ;;--------------------------------------------------
 ;; The C differential
 ;;--------------------------------------------------

 ;; The differential
 ((d-C * *) => *)
  
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element nil
	  0))

 ;; Unit element ring
 (local (defun unit nil
	  1))

 ;;--------------------------------------------------
 ;; D Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-D (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-D (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-D (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-D (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-D (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The D differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-D (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse C
 (local (defun inverse-C (n a)
	  (declare (ignore n a))
	  0))

 


 ;;--------------------------------------------------
 ;; The C differential
 ;;--------------------------------------------------
 
  ;; The differential
 (local (defun d-C (n a)
	  (declare (ignore n a))
	  0))


  ;;************************************************** 
  ;; Properties
  ;;************************************************** 
  

(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-c :group-operation-cc 'group-operation-c :zero-cc 'zero-c :external-cc 'external-c
		    :inverse-cc 'inverse-c :d-cc 'd-c)
 'C)


(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-d :group-operation-cc 'group-operation-d :zero-cc 'zero-d :external-cc 'external-d
		    :inverse-cc 'inverse-d :d-cc 'd-d)
 'D)

 
)
;;==================================================
;; The Direct Sum definitions
;;==================================================


 ;;--------------------------------------------------
 ;; Direct Sum Chain Complex 
 ;;--------------------------------------------------

 ;; Characteristic function
(defun inv-ds (n a) 
  (and (equal (list (car a) (cadr a)) a)
       (inv-C n (car a))
       (inv-D n (cadr a))     
       )
  )

 ;; Group Operation 
(defun group-operation-ds (n a b)
   (list (group-operation-C n (car a) (car b))
	 (group-operation-D n (cadr a) (cadr b))))
	  

 ;; Zero element
(defun zero-ds (n)
   (list (zero-C n)
	 (zero-D n)))
   

 ;; External multiplication
(defun external-ds (n a b)
   (list (external-C n a (car b))
	 (external-D n a (cadr b)))
	 )

 ;; Inverse element
(defun inverse-ds (n a)
   (list (inverse-C n (car a))
	 (inverse-D n (cadr a)))
   )
	 

 ;;--------------------------------------------------
 ;; Direct Sum differential 
 ;;--------------------------------------------------

 ;; The differential
(defun d-ds (n a)
  (list (d-C n (car a))
	(d-D n (cadr a))))


 ;;--------------------------------------------------
 ;; The Direct Sum is a Chain Complex 
 ;;--------------------------------------------------

(defthm group-operation-C-distrivutivity
  (implies (and (inv-c n a)
		(inv-c n b)
		(inv-c n c)
		(integerp n))
	   (equal (group-operation-c n a (group-operation-c n b c))
		  (group-operation-c n c (group-operation-c n a b))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |C-is-a-chain-complex|)))))



(defthm group-operation-D-distrivutivity
  (implies (and (inv-d n a)
		(inv-d n b)
		(inv-d n c)
		(integerp n))
	   (equal (group-operation-d n a (group-operation-d n b c))
		  (group-operation-d n c (group-operation-d n a b))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |D-is-a-chain-complex|)))))


(defthm inv-d-c
  (implies (and (inv-c n a) (integerp n))
	   (inv-c (+ n -1) (d-c n a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance |C-is-a-chain-complex|)))))

(defthm inv-d-c-bis
    (implies (and (inv-c n a) (integerp n))
	   (inv-c (+ -1 n) (d-c n a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance inv-d-c)))))



(defthm inv-d-d
  (implies (and (inv-d n a) (integerp n))
	   (inv-d (+ n -1) (d-d n a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance |D-is-a-chain-complex|)))))

(defthm inv-d-d-bis
    (implies (and (inv-d n a) (integerp n))
	   (inv-d (+ -1 n) (d-d n a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance inv-d-d)))))


(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-ds :group-operation-cc 'group-operation-ds :zero-cc 'zero-ds :external-cc 'external-ds
		    :inverse-cc 'inverse-ds :d-cc 'd-ds)
 'DIRECT-SUM-C-D)


(defthm correctness-ds
  (and (implies (and (integerp n)
		     (inv-ds n x))
		(and (equal (list (car x) (cadr x)) x)
		     (inv-C n (car x))
		     (inv-D n (cadr x))))
       (implies (integerp n)
		(equal (d-ds n a)
		       (list (d-C n (car a))
			     (d-D n (cadr a)))))))



;;;===========================================================================
;;;
;;; End of the direct sum construction
;;;
;;;===========================================================================




;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(inv-ds
   group-operation-ds
   zero-ds
   external-ds 
   inverse-ds
   d-ds
   |DIRECT-SUM-C-D-is-a-chain-complex|
   )
 )
|#


(defconst *ds*
  '((DEFUN INV-DS (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-C N (CAR A))
             (INV-D N (CADR A))))
 (DEFUN GROUP-OPERATION-DS (N A B)
        (LIST (GROUP-OPERATION-C N (CAR A) (CAR B))
              (GROUP-OPERATION-D N (CADR A)
                                 (CADR B))))
 (DEFUN ZERO-DS (N)
        (LIST (ZERO-C N) (ZERO-D N)))
 (DEFUN EXTERNAL-DS (N A B)
        (LIST (EXTERNAL-C N A (CAR B))
              (EXTERNAL-D N A (CADR B))))
 (DEFUN INVERSE-DS (N A)
        (LIST (INVERSE-C N (CAR A))
              (INVERSE-D N (CADR A))))
 (DEFUN D-DS (N A)
        (LIST (D-C N (CAR A)) (D-D N (CADR A))))
 (DEFTHM
  |DIRECT-SUM-C-D-is-a-chain-complex|
  (AND
   (AND
    (AND
      (AND (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                              (INV-RING (ADDITION-RING X Y)))
                     (IMPLIES (AND (INV-RING X)
                                   (INV-RING Y)
                                   (INV-RING Z))
                              (EQUAL (ADDITION-RING (ADDITION-RING X Y) Z)
                                     (ADDITION-RING X (ADDITION-RING Y Z)))))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING (ZERO-ELEMENT) X)
                                X))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING X (ZERO-ELEMENT))
                                X))
                (INV-RING (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING (INVERSE X) X)
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING X (INVERSE X))
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (INV-RING (INVERSE X))))
      (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                         (INV-RING (PRODUCT-RING X Y)))
                (IMPLIES (AND (INV-RING X)
                              (INV-RING Y)
                              (INV-RING Z))
                         (EQUAL (PRODUCT-RING (PRODUCT-RING X Y) Z)
                                (PRODUCT-RING X (PRODUCT-RING Y Z)))))
           (IMPLIES (INV-RING X)
                    (EQUAL (PRODUCT-RING (UNIT) X) X))
           (IMPLIES (INV-RING X)
                    (EQUAL (PRODUCT-RING X (UNIT)) X))
           (INV-RING (UNIT)))
      (IMPLIES (AND (INV-RING X)
                    (INV-RING Y)
                    (INV-RING Z))
               (EQUAL (PRODUCT-RING X (ADDITION-RING Y Z))
                      (ADDITION-RING (PRODUCT-RING X Y)
                                     (PRODUCT-RING X Z))))
      (IMPLIES (AND (INV-RING X)
                    (INV-RING Y)
                    (INV-RING Z))
               (EQUAL (PRODUCT-RING (ADDITION-RING X Y) Z)
                      (ADDITION-RING (PRODUCT-RING X Z)
                                     (PRODUCT-RING Y Z)))))
    (IMPLIES (AND (INV-DS N A)
                  (INV-DS N B)
                  (INTEGERP N))
             (INV-DS N (GROUP-OPERATION-DS N A B)))
    (IMPLIES (AND (INV-DS N A)
                  (INV-DS N B)
                  (INV-DS N C)
                  (INTEGERP N))
             (EQUAL (GROUP-OPERATION-DS N (GROUP-OPERATION-DS N A B)
                                        C)
                    (GROUP-OPERATION-DS N A (GROUP-OPERATION-DS N B C))))
    (INV-DS N (ZERO-DS N))
    (IMPLIES (AND (INV-DS N A)
                  (INV-RING R)
                  (INTEGERP N))
             (INV-DS N (EXTERNAL-DS N R A)))
    (IMPLIES (AND (INV-DS N A) (INTEGERP N))
             (EQUAL (GROUP-OPERATION-DS N A (ZERO-DS N))
                    A))
    (IMPLIES (AND (INV-DS N A) (INTEGERP N))
             (INV-DS N (INVERSE-DS N A)))
    (IMPLIES (AND (INV-DS N A)
                  (INV-DS N B)
                  (INTEGERP N)
                  (EQUAL (GROUP-OPERATION-DS N A B)
                         (ZERO-DS N)))
             (EQUAL (INVERSE-DS N A) B))
    (IMPLIES (AND (INV-DS N A) (INTEGERP N))
             (EQUAL (GROUP-OPERATION-DS N A (INVERSE-DS N A))
                    (ZERO-DS N)))
    (IMPLIES (AND (INV-DS N A)
                  (INV-DS N B)
                  (INTEGERP N))
             (EQUAL (GROUP-OPERATION-DS N A B)
                    (GROUP-OPERATION-DS N B A)))
    (IMPLIES (AND (INV-DS N A)
                  (INV-DS N B)
                  (INV-RING R)
                  (INTEGERP N))
             (EQUAL (EXTERNAL-DS N R (GROUP-OPERATION-DS N A B))
                    (GROUP-OPERATION-DS N (EXTERNAL-DS N R A)
                                        (EXTERNAL-DS N R B))))
    (IMPLIES (AND (INV-DS N A)
                  (INV-RING S)
                  (INV-RING R)
                  (INTEGERP N))
             (EQUAL (EXTERNAL-DS N (ADDITION-RING S R) A)
                    (GROUP-OPERATION-DS N (EXTERNAL-DS N S A)
                                        (EXTERNAL-DS N R A))))
    (IMPLIES (AND (INV-DS N A)
                  (INV-RING S)
                  (INV-RING R)
                  (INTEGERP N))
             (EQUAL (EXTERNAL-DS N (PRODUCT-RING S R) A)
                    (EXTERNAL-DS N S (EXTERNAL-DS N R A))))
    (IMPLIES (AND (INV-DS N A) (INTEGERP N))
             (EQUAL (EXTERNAL-DS N (UNIT) A) A))
    (IMPLIES (AND (INV-DS N A)
                  (INV-DS N B)
                  (INTEGERP N))
             (EQUAL (INVERSE-DS N (GROUP-OPERATION-DS N A B))
                    (GROUP-OPERATION-DS N (INVERSE-DS N A)
                                        (INVERSE-DS N B))))
    (IMPLIES (AND (INV-DS N A)
                  (INV-RING S)
                  (INTEGERP N))
             (EQUAL (INVERSE-DS N (EXTERNAL-DS N S A))
                    (EXTERNAL-DS N S (INVERSE-DS N A))))
    (IMPLIES (INTEGERP N)
             (EQUAL (INVERSE-DS N (ZERO-DS N))
                    (ZERO-DS N)))
    (IMPLIES (AND (INV-RING S) (INTEGERP N))
             (EQUAL (EXTERNAL-DS N S (ZERO-DS N))
                    (ZERO-DS N))))
   (AND (AND (IMPLIES (AND (INV-DS N A) (INTEGERP N))
                      (INV-DS (+ N -1) (D-DS N A)))
             (IMPLIES (AND (INV-DS N A)
                           (INV-DS N B)
                           (INTEGERP N))
                      (EQUAL (D-DS N (GROUP-OPERATION-DS N A B))
                             (GROUP-OPERATION-DS (+ N -1)
                                                 (D-DS N A)
                                                 (D-DS N B))))
             (IMPLIES (AND (INV-DS N A)
                           (INV-RING R)
                           (INTEGERP N))
                      (EQUAL (D-DS N (EXTERNAL-DS N R A))
                             (EXTERNAL-DS (+ N -1) R (D-DS N A))))
             (IMPLIES (INTEGERP N)
                      (EQUAL (D-DS N (ZERO-DS N))
                             (ZERO-DS (+ N -1))))
             (IMPLIES (AND (INV-DS N A) (INTEGERP N))
                      (EQUAL (D-DS N (INVERSE-DS N A))
                             (INVERSE-DS (+ N -1) (D-DS N A)))))
        (IMPLIES (AND (INV-DS N A) (INTEGERP N))
                 (EQUAL (D-DS (1- N) (D-DS N A))
                        (ZERO-DS (1- (1- N)))))))))
)


(make-generic-theory *ds*)












